FDL - Nuprl Lemma : strict-fun-connected-induction

Nuprl Lemma : strict-fun-connected-induction

T:Type, f:(T

T), R:(T

T

).
(

x, y, z:T. (x = f(y))

(

(x = y))

y is f*(z)

(R(y,z)

(y = z))

R(x,z))

{

x, y:T. x = f+(y)

R(x,y)}

Definitions t T, x:AB(x), Type, f(a), , , left + right, A, <a, b>, Void, False, x:A B(x), x:A. B(x), hd(l), y=f*(x) via L, Dec(P), P & Q, P Q, , a < b, A B, Atom, {i..j}, b, x,y:A//B(x;y), b | a, a ~ b, |p|, a b, a <p b, |g|, a < b, A c B, x f y, |r|, xL. P(x), (xL.P(x)), Unit, , , rel_exp(T;R;n), (x l), type List, {T}, x.A(x), x,y. t(x;y), y = f+(x), s = t, x(s1,s2), P Q, y is f*(x), P Q, x:A. B(x)

Lemmas strict-fun-connected wf, fun-connected-induction, fun-connected wf, not wf